\begin{tabbing}
(\=(ExRepD$\cdot$) \+
\\[0ex]CollapseTHEN ((((if (((first\_nat 2:n)) = 0) then (Repeat (MoveToConcl ({-}1)
\-\\[0ex])\=) else (RepeatFor (first\_nat 2:n) (MoveToConcl ({-}1))))$\cdot$) \+
\\[0ex]CollapseTHEN (((
\-\\[0ex]C\=ompleteInductionOnNat) \+
\\[0ex]CollapseTHEN (((Auto$\cdot$) 
\\[0ex]CollapseTHEN (((Decide $\exists$$i$:\{0..$n$$^{-}$\}\=\+
\\[0ex]($\uparrow$($P$($i$))) 
\-\\[0ex]$\cdot$)
\\[0ex]
\-\\[0ex]CollapseTHENA (Auto$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$
\end{tabbing}